YES 0.808 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ LR

mainModule Main
  ((exponent :: Float  ->  Int) :: Float  ->  Int)

module Main where
  import qualified Prelude



Lambda Reductions:
The following Lambda expression
\(m,_)→m

is transformed to
m0 (m,_) = m

The following Lambda expression
\(_,n)→n

is transformed to
n0 (_,n) = n



↳ HASKELL
  ↳ LR
HASKELL
      ↳ IFR

mainModule Main
  ((exponent :: Float  ->  Int) :: Float  ->  Int)

module Main where
  import qualified Prelude



If Reductions:
The following If expression
if m == 0 then 0 else n + floatDigits x

is transformed to
exponent0 x True = 0
exponent0 x False = n + floatDigits x



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
HASKELL
          ↳ BR

mainModule Main
  ((exponent :: Float  ->  Int) :: Float  ->  Int)

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
HASKELL
              ↳ COR

mainModule Main
  ((exponent :: Float  ->  Int) :: Float  ->  Int)

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
HASKELL
                  ↳ LetRed

mainModule Main
  ((exponent :: Float  ->  Int) :: Float  ->  Int)

module Main where
  import qualified Prelude



Let/Where Reductions:
The bindings of the following Let/Where expression
exponent0 x (m == 0)
where 
exponent0 x True = 0
exponent0 x False = n + floatDigits x
m  = m0 vu10
m0 (m,vv) = m
n  = n0 vu10
n0 (vw,n) = n
vu10  = decodeFloat x

are unpacked to the following functions on top level
exponentExponent0 ww x True = 0
exponentExponent0 ww x False = exponentN ww + floatDigits x

exponentM ww = exponentM0 ww (exponentVu10 ww)

exponentN0 ww (vw,n) = n

exponentVu10 ww = decodeFloat ww

exponentM0 ww (m,vv) = m

exponentN ww = exponentN0 ww (exponentVu10 ww)



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
HASKELL
                      ↳ NumRed

mainModule Main
  ((exponent :: Float  ->  Int) :: Float  ->  Int)

module Main where
  import qualified Prelude



Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
HASKELL
                          ↳ Narrow

mainModule Main
  (exponent :: Float  ->  Int)

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNat(Succ(wx110), Succ(wx1000)) → new_primMinusNat(wx110, wx1000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(wx700), Succ(wx80)) → new_primPlusNat(wx700, wx80)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: